es:ES, T:Type, I:MaInterface(T), i:Id.
(i  ma-interface-locs(I))  (e:E. (loc(e) = i)  ([[I|i]](e) ~ [[I]](e))) 

latex

Definitions

do-apply(f;x), ma-interface-val(es;X;e), ma-in-interface(es;X;e), es-triggers(es;i;ds;conds), X(e), [[X]], [[I|i]], t  T, x:A. B(x), loc(e), s = t, , Id, P  Q, E, (x  l), MaInterface(T), Type, ES, {T}, SQType(T), Atom$n, tt, IdDeq, x  dom(f), s ~ t, ma-interface-locs(I), P  Q, P & Q, P  Q, x:A  B(x), b, a:A fp B(a), a < b, t.1, {x:A| B(x)} , Knd, Top, left + right, x:AB(x), State(ds), hasloc(k;i), x. t(x), x.A(x), <a, b>, , False, A, f(x), let x,y = A in B(x;y), t.2, f(a), outl(x), Unit, ff, if b then t else f fi , kind(e), ma-interface-domb(I;i;k), ma-interface-dom(I;i), type List, Void, x:A.B(x), x:A. B(x), S  T, IdLnk, fpf-domain(f), #$n, ||as||, A  B, , , l[i], A c B, KindDeq

Lemmas

length wf nat, nat wf, select wf, IdLnk wf, fpf-domain wf, subtype rel product, subtype rel list, subtype rel function, subtype rel set, l member wf, subtype-set-hasloc, fpf-ap wf, assert-ma-interface-domb, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bool sq, eqtt to assert, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, Id wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, member-fpf-dom, Id sq, es-loc wf